M1, M2, M3:MsgA. M1  M2  M2  M3  M1  M3 

latex

Definitions	x:A. B(x), P  Q, M1  M2, State(ds), Valtype(da;k), Prop, 1of(t), 2of(t), A & B, P & Q, t  T, x. t(x), MsgA, x(s), {T}
Lemmas	fpf-sub transitivity, Id wf, id-deq wf, Knd wf, Kind-deq wf, fpf-sub functionality, strong-subtype-self, fpf-cap wf, subtype-fpf2, subtype-fpf-cap-void, ma-state wf, locl wf, top wf, subtype rel function, subtype rel dep function, subtype rel self, subtype-fpf-cap-top, pi1 wf, pi2 wf, product-deq wf, IdLnk wf, rcv wf, idlnk-deq wf, subtype rel list, subtype rel product, ma-sub wf, msga wf